/*
 * Atomic Predicates for Transformers
 * 
 * Copyright (c) 2015 UNIVERSITY OF TEXAS AUSTIN. All rights reserved. Developed
 * by: HONGKUN YANG and SIMON S. LAM http://www.cs.utexas.edu/users/lam/NRL/
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * with the Software without restriction, including without limitation the
 * rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
 * sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * 1. Redistributions of source code must retain the above copyright notice,
 * this list of conditions and the following disclaimers.
 * 
 * 2. Redistributions in binary form must reproduce the above copyright notice,
 * this list of conditions and the following disclaimers in the documentation
 * and/or other materials provided with the distribution.
 * 
 * 3. Neither the name of the UNIVERSITY OF TEXAS AUSTIN nor the names of the
 * developers may be used to endorse or promote products derived from this
 * Software without specific prior written permission.
 * 
 * 4. Any report or paper describing results derived from using any part of this
 * Software must cite the following publication of the developers: Hongkun Yang
 * and Simon S. Lam, Scalable Verification of Networks With Packet Transformers
 * Using Atomic Predicates, IEEE/ACM Transactions on Networking, October 2017,
 * Volume 25, No. 5, pages 2900-2915 (first published as IEEE Early Access
 * Article, July 2017, Digital Object Identifier: 10.1109/TNET.2017.2720172).
 * 
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH
 * THE SOFTWARE.
 */
package transformer;

import java.io.*;
import java.lang.management.*;
import java.util.*;

import common.PositionTuple;



public class StateTransferI2Run {

      public static void compute_trees(Net net, Set<PositionTuple> pts, PrintWriter pw)
      {
            compute_trees(net, pts, pw, false);
      }

      public static void compute_trees2(Net net, Set<PositionTuple> pts, PrintWriter pw)
      {
            //final ThreadMXBean threadMX = ManagementFactory.getThreadMXBean();
            //assert threadMX.isCurrentThreadCpuTimeSupported();
            //threadMX.setThreadCpuTimeEnabled(true);

            StateTransfer stfer = new StateTransfer(net);
            int repeat = 1;
            //long t1 = threadMX.getCurrentThreadCpuTime();
            long t1 = System.nanoTime();
            for (int i = 0; i < repeat; i++)
            {
                  for(PositionTuple pt1 : pts)
                  {
                        StateBDD hs = stfer.Traverse(pt1);      
                        //hs.printState();
                  }
            }
            //long t2 = threadMX.getCurrentThreadCpuTime();
            long t2 = System.nanoTime();
            pw.println((t2-t1+0.0)/1000000.0/repeat);
      }
      
      public static double compute_trees_anypkt(Net net, Set<PositionTuple> pts, PrintWriter pw)
      {
            //final ThreadMXBean threadMX = ManagementFactory.getThreadMXBean();
            //assert threadMX.isCurrentThreadCpuTimeSupported();
            //threadMX.setThreadCpuTimeEnabled(true);

            StateTransfer stfer = new StateTransfer(net);
            int repeat = 1;
            //long t1 = threadMX.getCurrentThreadCpuTime();
            long t1 = System.nanoTime();
            for (int i = 0; i < repeat; i++)
            {
                  for(PositionTuple pt1 : pts)
                  {
                        StateBDD hs = stfer.TraverseAnyPkt(pt1);      
                        //hs.printState();
                  }
            }
            //long t2 = threadMX.getCurrentThreadCpuTime();
            long t2 = System.nanoTime();
            double elapse = (t2-t1+0.0)/1000000.0/repeat;
            if(pw != null)
                  pw.println(elapse);
            return elapse;
      }
      
      public static double compute_trees_anynonmplspkt(Net net, Set<PositionTuple> pts, PrintWriter pw)
      {
          StateTransfer stfer = new StateTransfer(net);
          int repeat = 1;
          long t1 = System.nanoTime();
          for (int i = 0; i < repeat; i++)
          {

                for(PositionTuple pt1 : pts)
                {
                      StateBDD hs = stfer.TraverseAnyNonMPLSPkt(pt1);      
                      
                }
          }
          long t2 = System.nanoTime();
          double elapse = (t2-t1+0.0)/1000000.0/repeat;
          if(pw != null)
                pw.println(elapse);
          return elapse;
      }
      
      public static double compute_trees_anynontunnelpkt(Net net, Set<PositionTuple> pts, PrintWriter pw)
      {

            StateTransfer stfer = new StateTransfer(net);
            int repeat = 1;
            long t1 = System.nanoTime();
            for (int i = 0; i < repeat; i++)
            {
                 // int cnt = 0;
                 // int thres = 0;
                  for(PositionTuple pt1 : pts)
                  {
                        //System.out.println(pt1);
                        //cnt ++;
                       // if(cnt < thres)
                        //{
                        //      continue;
                        //}
                        StateBDD hs = stfer.TraverseAnyNonTunnelPkt(pt1);      
                        
                        
                        //System.out.println("port #"+cnt);
                        //hs.printState();
                        /*
                        
                        if(cnt == 2)
                        {
                              break;
                        }*/
                  }
            }
            long t2 = System.nanoTime();
            double elapse = (t2-t1+0.0)/1000000.0/repeat;
            if(pw != null)
                  pw.println(elapse);
            return elapse;
      }

      public static void compute_trees3(Net net, Set<PositionTuple> pts, PrintWriter pw)
      {
            final ThreadMXBean threadMX = ManagementFactory.getThreadMXBean();
            assert threadMX.isCurrentThreadCpuTimeSupported();
            threadMX.setThreadCpuTimeEnabled(true);

            StateTransfer stfer = new StateTransfer(net);
            int repeat = 1;
            StateUtility su = new StateUtility();
            long t1 = threadMX.getCurrentThreadCpuTime();
            for (int i = 0; i < repeat; i++)
            {
                  for(PositionTuple pt1 : pts)
                  {
                        StateBDD hs = stfer.Traverse(pt1);
                        su.add_state(hs);
                  }
            }
            long t2 = threadMX.getCurrentThreadCpuTime();
            pw.println((t2-t1)/1000000.0/repeat);
            pw.println("average num of nodes: "+su.get_ave_num_nodes());
      }


      public static void compute_trees(Net net, Set<PositionTuple> pts, PrintWriter pw, boolean cputime)
      {
            if(cputime)
            {
                  compute_trees3(net, pts, pw);
            }else
            {
                  compute_trees2(net, pts, pw);
            }
      }

      /**
       * 
       * @param args - 1,2,3
       * @throws IOException
       */
      public static void main(String[] args) throws IOException
      {
            Network n = new Network("i2", true);
            StateTransfer stfer = new StateTransfer(n);
            Set<PositionTuple> pts = n.getallactiveports();
            System.out.println(pts.size() + " ports in total");

            StateUtility su = new StateUtility();

            for(PositionTuple pt1 : pts)
            {
                  long t1 = System.nanoTime();
                  StateBDD hs = stfer.TraverseCombPkt(pt1);
                  long t2 = System.nanoTime();
                  System.out.println((t2-t1)/1000000.0);
                  su.add_state(hs);
                  //hs.printState();
            }

            //su.show_heights();
            //su.show_num_leaves();

            System.out.println("average heights:" + su.get_ave_height());
            double [] height_order = su.get_order_height();
            System.out.println("median heights:" + height_order[1]);
            System.out.println("max heights:" + height_order[2]);

            System.out.println("average num of leaves:" + su.get_ave_num_leaves());
            double [] leave_order = su.get_order_leaves();
            System.out.println("median of leaves:" + leave_order[1]);
            System.out.println("max leaves:" + leave_order[2]);



      }
}
